Skip to content

refactor(LinearAlgebra/Orientation,LinearAlgebra/AffineSpace/FiniteDimensional): instances for arbitrary orientations#39696

Open
jsm28 wants to merge 4 commits into
leanprover-community:masterfrom
jsm28:arbitrary-orientation
Open

refactor(LinearAlgebra/Orientation,LinearAlgebra/AffineSpace/FiniteDimensional): instances for arbitrary orientations#39696
jsm28 wants to merge 4 commits into
leanprover-community:masterfrom
jsm28:arbitrary-orientation

Conversation

@jsm28

@jsm28 jsm28 commented May 22, 2026

Copy link
Copy Markdown
Contributor

Based on suggestions by @kim-em on Zulip https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/PRs.20towards.20IMO.20geometry.202024.20P4/near/596946072 add convenience scoped instances for choosing an arbitrary orientation of a module, and for the finrank of the span of the vertices of a simplex.

Note: I don't understand why the latter scoped instance is only found automatically in one of the two places using it; in Sphere/Power.lean it's necessary to use Affine.Simplex.fact_finrank_direction_affineSpan_eq rather than relying on typeclass inference, but in Angle/Sphere.lean typeclass inference suffices.

Open in Gitpod

@jsm28
refactor(LinearAlgebra/Orientation,LinearAlgebra/AffineSpace/FiniteDi…
6470e9c 
…mensional): instances for arbitrary orientations

Based on suggestions by @kim-em on Zulip https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/PRs.20towards.20IMO.20geometry.202024.20P4/near/596946072 add convenience scoped instances for choosing an arbitrary orientation of a module, and for the `finrank` of the span of the vertices of a simplex.

Note: I don't understand why the latter scoped instance is only found automatically in one of the two places using it; in `Sphere/Power.lean` it's necessary to use `Affine.Simplex.fact_finrank_direction_affineSpan_eq` rather than relying on typeclass inference, but in `Angle/Sphere.lean` typeclass inference suffices.
@jsm28 jsm28 added t-algebra Algebra (groups, rings, fields, etc) t-euclidean-geometry Affine and axiomatic geometry labels May 22, 2026
@github-actions

github-actions Bot commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 89e72691fb

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

- someOrientation

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- unavailable)

⚠️ The Mathlib cache for this PR's merge-base isn't on the server (typically a bors-batch intermediate that CI never built). Merge master into this PR and push to refresh.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 89e72691fb
Reference commit 9944fe2973

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented May 23, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 23, 2026
@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 23, 2026
@jsm28 jsm28 mentioned this pull request Jul 3, 2026
Open
10 tasks
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 14, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented Jul 14, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 14, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 17, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented Jul 17, 2026

Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 17, 2026
@jsm28 jsm28 mentioned this pull request Jul 20, 2026
Open
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@eric-wieser eric-wieser

Labels

t-algebra Algebra (groups, rings, fields, etc) t-euclidean-geometry Affine and axiomatic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jsm28 @eric-wieser